mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props actuators -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --alg OptimisticValueIteration --epsilon 5e-2 --width 5e-2 --relative-width --p0 --p1
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.
Peak memory usage: 53 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0
+ State space exploration
State size: 16 bytes
States: 5820
Transitions: 5820
Branches: 16788
Rate: 83143 states/s
Time: 0.1 s
+ Property actuators
Probability: 0.10706854653165529
Bounds: [0.10318017195622811, 0.11095692110708245]
Time: 6.2 s
+ Precomputations
Min. prob. 0 states: 4512
Time for min. prob. 0 states: 0.0 s
Min. prob. 1 states: 180
Time for min. prob. 1 states: 0.0 s
+ Essential states
Iterations: 1
Essential states: 1130
Transitions: 1130
Branches: 7386
Time: 0.0 s
+ Optimistic value iteration
Total iterations: 91881
Verif. attempts: 13
Verif. iterations: 33757
Final epsilon: 2.447969165540277E-06
Time: 6.2 s
Exported results to file "/out.txt".